This invention relates to a process and system for developing mathematically validated object oriented software.
Most computer programs contain bugs (i.e. software errors). In general it may be said that a program contains a bug if the executing program fails to meet the user requirements that it was intended to satisfy. Bugs may be introduced at various stages of the software development process:                1. The user's requirements may not have been correctly understood and documented;        2. The system specification that was written may not perform in accordance with the documented user requirements;        3. The system design may fail to conform to the specification;        4. Components used to implement the design may by assembled in ways that violate the safe conditions for use of the components;        5. Components may have been incorrectly programmed and so fail to perform correctly even when assembled correctly;        6. Correctly written components may have been translated incorrectly to machine language.        
It is desirable to provide early detection of bugs introduced in all of these stages and to provide final product certainty, or near certainty, that the program will behave according to its specifications. To this end, the following are described in the prior art: specification languages (including object-oriented specification languages); object-oriented programming languages; a system that validates older (non-object-oriented) specifications and program descriptions by generating proof obligations; and automated proof techniques.
However, the prior art in this field does not address the problems of specifying and verifying the behaviour of programs using object-oriented techniques including inheritance and dynamic binding.